package alloy.viz.alloyviz;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;

import alloy.api.SolutionData;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.util.Dbg;

/**
 * @deprecated
 * THIS CLASS IS DEPRECATED, AND IT MAY PRODUCE INACCURATE MODELS.
 * 
 * This wrapper is designed to convert the information from
 * SolutionData.java in the old alloy analyzer into information used
 * by newalloyviz. The process involves extracting the model and
 * instance from SolutionData.
 * 
 * Note: This is really a utility class, probably doesn't even need to
 * be public
 */
public class SolutionDataWrapper {
  
    private SolutionData solutionData;

    // The extracted Model
    private Model model;
    
    // The extracted Instance
    private VizInstance instance;

    // The List of types (BasicType)
    //private List basicTypes;

    // The List of Sets (Sigs)
    //private List sigs;

    // Set of all ModuleNames
    private List modules;

    // The Mapping of Module names to associated TypeStructures
    private Map modulesToTypes;

    // The Mapping of Module names to associated Lists of AlloySets
    private Map modulesToSets;

    // The Mapping of Module names to associated AlloyRelations The value
    // of the mapping are lists of AlloyRelations (includes skolem
    // constants for now)
    private Map modulesToRelations;

    // Mapping of Module names to associatd skolem relations. The module name
    // is based on the first type of the skolem relation.
    //private Map modulesToSkolemRelations;

    // Map of Basic Types to AlloyTypes, the sigs must be a basic type or it
    // will not exist in the map.
    // The sig names are Fully qualified names as defined in SolutionData
    private Map typesToAlloyTypes;
    
    // Map of Sig Names to AlloySets, the sigs must not be a basic type
    // The sig names are fully qualified names
    private Map sigsToAlloySets;

    // Map of relation names in SolutionData to AlloyRelations
    // The relation names in SolutionData are fully qualified
    private Map relationsToAlloyRelations;

    // Mapping of skolem constants to AlloyRelations Skolem names are
    // also fully qualified as defined in SolutionData
    private Map skolemsToAlloyRelations;

    // Map of SolutionData atom names to AlloyAtoms
    private Map atomsToAlloyAtoms;

    // Mapping of skolem names to AlloySets. In our model, a unary relation
    // is a set, so a skolem constant with only tuple is considered a set
    private Map skolemsToAlloySets;
    
    
    /**
     * @deprecated
     * Creates a wrapper for the input SolutionData.
     */
    public SolutionDataWrapper(SolutionData solutionData) {
	
	this.solutionData = solutionData;
	//basicTypes = new LinkedList();
	//sigs = new LinkedList();
	//modules = new HashSet();
	modules = new ArrayList();
	modulesToTypes = new HashMap();
	modulesToSets = new HashMap();
	modulesToRelations = new HashMap();
	typesToAlloyTypes = new HashMap();
	sigsToAlloySets = new HashMap();
	relationsToAlloyRelations = new HashMap();
	skolemsToAlloyRelations = new HashMap();
	atomsToAlloyAtoms = new HashMap();
	skolemsToAlloySets = new HashMap();

	generateModel();
	generateInstance();
    }

    /**
     * @deprecated
     * Return the generated newalloyviz.alloyviz.Model.
     */
    public Model getGeneratedModel() {
	return model;
    }

    /**
     * @deprecated
     * Return the generated newalloyviz.alloyviz.Instance.
     */
    public VizInstance getGeneratedInstance() {
	return instance;
    }

    // Extract the model from SolutionData.
    private void generateModel() {
	
	// Get the types
	// For the moment, there is no type structure since subtyping
	// is not yet completed.
	// This contains just the "basic types" in SolutionData
	for (Iterator types = solutionData.allTypes().iterator();types.hasNext();) {
	    String longTypeName = ((BasicType)types.next()).toString();
	    
	    //System.out.println("TypeName: " + longTypeName);

	    //String shortTypeName = solutionData.getShortName(longTypeName);
	    String shortTypeName = solutionData.getShortName(longTypeName);
	    //System.out.println("Long Type Name: " + longTypeName);
	    //System.out.println("Short Type Name: " + shortTypeName);
	    String moduleName = getModuleName(longTypeName);
	    //System.out.println("Module name of basic type: " + moduleName);
	    if (!modules.contains(moduleName))
	    	modules.add(moduleName);
	    
	    //modules.add(moduleName);
	    AlloyType newType = new AlloyType(shortTypeName);
	    typesToAlloyTypes.put(longTypeName,newType);
	    //System.out.println ("Putting long type name: " + longTypeName);
	    if(modulesToTypes.containsKey(moduleName)) {
		TypeStructure associatedTypes = (TypeStructure)(modulesToTypes.get(moduleName));
		associatedTypes.addType(newType);
	    }
	    else {
		TypeStructure associatedTypes = new TypeStructure();
		associatedTypes.addType(newType);
		modulesToTypes.put(moduleName,associatedTypes);
	    }
	}
	    
	//System.out.println(modules);
	// Get the sets
	for (Iterator sigs = solutionData.allSigs().iterator(); sigs.hasNext();) {
	    String longSigName = (String)sigs.next();

	    // can't seem to extract the module from the sig name
	    //String typeName = solutionData.typeOfSig(longSigName).toString();
	    //System.out.println(longSigName);
	    //String moduleName = getModuleName(longSigName);
	    //modules.add(moduleName);
	    String shortSigName = solutionData.getShortName(longSigName);
	    Dbg.check(shortSigName);

	    // if it's a basic type, it should have been taken care of above
	    if(!solutionData.isBasic(longSigName)) {
		String typeOfSig = solutionData.typeOfSig(longSigName).toString();
		//String shortTypeOfSig = solutionData.getShortName(typeOfSig);
		//System.out.println ("Looking up: " + shortTypeOfSig);
		AlloyType setType = (AlloyType)typesToAlloyTypes.get(typeOfSig);
		String moduleName = getModuleName(typeOfSig);
		//System.out.println("Module name of Sig:" + moduleName);
		
		if(!modules.contains(moduleName)) {
		    Dbg.fail("Module " + moduleName + " should have been added previously.");
		}

		Dbg.check(setType);
		AlloySet newSet = new AlloySet(shortSigName,setType);
		sigsToAlloySets.put(longSigName, newSet);
		if(modulesToSets.containsKey(moduleName)) {
		    List associatedSets = (List)(modulesToSets.get(moduleName));
		    associatedSets.add(newSet);
		}
		else {
		    List associatedSets = new LinkedList();
		    associatedSets.add(newSet);
		    modulesToSets.put(moduleName, associatedSets);
		}
	    }
	    else if(solutionData.isBasic(longSigName)) {
		String longTypeName = solutionData.typeOfSig(longSigName).toString();
		if(!typesToAlloyTypes.containsKey(longTypeName)) {
		    Dbg.fail("Basic type " + longSigName + " is not in a TypeStructure!");
		}
		//System.out.println("finished with: " + longSigName);
	    }
	    else {
		Dbg.fail("Error in creating AlloySets for Sigs in SolutionData!");
	    }
	}

	// Get the relations (using RelationType)
	Map relations = solutionData.allRelations();
	List alloyRelations;
	List types;
	for (Iterator relationNames = relations.keySet().iterator(); relationNames.hasNext();) {
	    String relationName = (String)relationNames.next();
	    String shortRelationName = getShortRelationName(solutionData.getShortName(relationName));
	    //System.out.println(relationName);
	    String moduleName = getRelationModuleName(relationName);
	    //System.out.println(moduleName);
	    
	    if(!modules.contains(moduleName)) {
		Dbg.fail("Module " + moduleName + " should have been added previously.");
	    }

	    //modules.add(moduleName);
	    RelationType relationType = (RelationType)relations.get(relationName);
	    types = new LinkedList();
	    for(int i = 0;i < relationType.numBasicTypes();i++) {
		String longTypeName = relationType.getBasicTypeAt(i).toString();
		String shortTypeName = solutionData.getShortName(longTypeName);
		types.add(typesToAlloyTypes.get(longTypeName));
	    }

	    AlloyRelation rel = new AlloyRelation(shortRelationName,types);
	    relationsToAlloyRelations.put(relationName,rel);

	    if(modulesToRelations.containsKey(moduleName)) {
		alloyRelations = (List)modulesToRelations.get(moduleName);
		alloyRelations.add(rel);
	    }
	    else {
		alloyRelations = new LinkedList();
		alloyRelations.add(rel);
		modulesToRelations.put(moduleName, alloyRelations);
	    }

	    //System.out.println("Finished with: " + relationName);
	}

	// Skolem constants - Do these really belong in the model? 
	// (For now, "yes")
	Map skolemConstants = solutionData.skolemConstants();
	List skolemRelationTypes;
	String moduleName;
	for(Iterator skolems = skolemConstants.entrySet().iterator(); skolems.hasNext();) {
	    Map.Entry skolemEntry = (Map.Entry)skolems.next();
	    String skolemName = (String)skolemEntry.getKey();
	    RelationType skolemType = (RelationType)skolemEntry.getValue();
	    skolemRelationTypes = new LinkedList();

	    // the module name is based on the first type of the relation
	    moduleName = getModuleName(skolemType.getBasicTypeAt(0).toString());
	    //System.out.println(moduleName);
	   
	    if(!modules.contains(moduleName)) {
		Dbg.fail("Module " + moduleName + " should have been added previously.");
	    }
	    //modules.add(moduleName);

	    // in our model (newalloyviz), a unary relation is treated as a set rather than a relation
	    if(skolemType.numBasicTypes() == 1) {
		String longTypeName = skolemType.getBasicTypeAt(0).toString();
		AlloySet skolemSet = new AlloySet(skolemName,(AlloyType)typesToAlloyTypes.get(longTypeName));
		skolemsToAlloySets.put(skolemName, skolemSet);
		if(modulesToSets.containsKey(moduleName)) {
		    List associatedSets = (List)(modulesToSets.get(moduleName));
		    associatedSets.add(skolemSet);
		}
		else {
		    List associatedSets = new LinkedList();
		    associatedSets.add(skolemSet);
		    modulesToSets.put(moduleName, associatedSets);
		}
	    }
	    else {
		for(int i=0;i<skolemType.numBasicTypes();i++) {
		    String longTypeName = skolemType.getBasicTypeAt(i).toString();
		    //String shortTypeName = solutionData.getShortName(longTypeName);
		    skolemRelationTypes.add(typesToAlloyTypes.get(longTypeName));
		}
		if(!modulesToRelations.containsKey(moduleName)) {
		    //so apparently, you can get just skolem relations in a model (did not know that was possible) 
		    alloyRelations = new LinkedList();
		    AlloyRelation skolemRelation = new AlloyRelation(skolemName,skolemRelationTypes);
		    alloyRelations.add(skolemRelation);
		    skolemsToAlloyRelations.put(skolemName,skolemRelation);
		    modulesToRelations.put(moduleName, alloyRelations);
		}
		else {
		    AlloyRelation skolemRelation = new AlloyRelation(skolemName,skolemRelationTypes);
		    skolemsToAlloyRelations.put(skolemName,skolemRelation);
		    alloyRelations = (List)modulesToRelations.get(moduleName);
		    alloyRelations.add(skolemRelation);
		}
	    }
	}

	// Create the modules
	List alloyModules = new LinkedList();
	for(Iterator moduleNames = modules.iterator(); moduleNames.hasNext();) {
	    String name = (String)moduleNames.next();
	    //System.out.println(name);
	    TypeStructure mtypes = (TypeStructure)modulesToTypes.get(name);
	    //System.out.println(mtypes);
	    List msets;
	    if(!modulesToSets.containsKey(name)) {
		msets = new LinkedList();
	    }
	    else {
		msets = (List)modulesToSets.get(name);
	    }

	    //System.out.println(msets);
	    List mrels;
	    if(!modulesToRelations.containsKey(name)) {
		 //System.out.println(name);
		 mrels = new LinkedList();
	    }
	    else {
		 //System.out.println(name);
		 mrels = (List)modulesToRelations.get(name);
	    }
	    //List mrels = (List)modulesToRelations.get(name);

	    //System.out.println(mrels);
	    AlloyModule module = new AlloyModule(name, mtypes.getTypes(), msets, mrels);
	    alloyModules.add(module);
	}

	// Generate the Model
	// get the name from the first module (should be correct)
	String modelName;
	if(!modules.isEmpty()) {
	     modelName = (String) modules.iterator().next();
	}
	else {
	     modelName = "*";
	}
	model = new Model(alloyModules, new TypeStructure(), modelName);
    }


    // extract the Instance from SolutionData
    private void generateInstance() {
	instance = new VizInstance(model);
	
	// Get the atoms
	AlloyAtom atom;
	String sdAtomName;
	for(Iterator sigs = solutionData.allSigs().iterator();sigs.hasNext();) {
	    String sigName = (String)sigs.next();
	    List atoms = solutionData.atomsOfSig(sigName);

	    for(Iterator atomsIterator = atoms.iterator();atomsIterator.hasNext();) {
		sdAtomName = (String)atomsIterator.next();
		String atomName = getAtomName(sdAtomName);
		int atomIndex = getAtomIndex(sdAtomName);
		
		if(solutionData.isBasic(sigName)) {
		    // basic type, no sets
		    //System.out.println(sigName);
		    //System.out.println((AlloyType)sigsToAlloyTypes.get(sigName));		    
		    String longTypeName = solutionData.typeOfSig(sigName).toString();
		    atom = new AlloyAtom(sdAtomName,(AlloyType)typesToAlloyTypes.get(longTypeName),atomIndex);
		    atomsToAlloyAtoms.put(sdAtomName,atom);
		    if (!instance.containsAtom(atom)) {
			instance.addAtom(atom);
		    }
		}
		else {		    
		    // a set with a basic type		    
		    AlloySet set = (AlloySet)sigsToAlloySets.get(sigName);
		    AlloyType setType = set.getType();
		    atom = new AlloyAtom(sdAtomName, setType, atomIndex);
		    atomsToAlloyAtoms.put(sdAtomName,atom);
		    if (!instance.containsAtom(atom)) {
			instance.addAtom(atom);
		    }
		    instance.addAtomToSet(atom,set);
		}		
	    }
	    
	}

	//System.out.println(instance);
	
	// Get the relations
	Map relations = solutionData.allRelations();
	for(Iterator relationsIterator = relations.keySet().iterator();relationsIterator.hasNext();) {
	    String relationName = (String)relationsIterator.next();
	    AlloyRelation alloyRelation = (AlloyRelation)relationsToAlloyRelations.get(relationName);
	    
	    for(Iterator tuples=solutionData.tuplesOfRelation(relationName).iterator();tuples.hasNext();) {
		String[] atomsOfRelation = (String[])tuples.next();
		List alloyAtoms = new LinkedList();
		for(int i = 0;i<atomsOfRelation.length;i++) {
		    atom = (AlloyAtom)atomsToAlloyAtoms.get(atomsOfRelation[i]);
		    alloy.util.Dbg.chk(atom, "no AlloyAtom for: "+atomsOfRelation[i]);
		    alloyAtoms.add(atom);
		}
		instance.addTupleToRelation(new AlloyTuple(alloyAtoms),alloyRelation);
	    }
	}

	// Get Skolem constant relations
	for (Iterator skolemNames = skolemsToAlloySets.keySet().iterator();skolemNames.hasNext();) {
	    String skolem = (String)skolemNames.next();
	    for(Iterator tuples = solutionData.skolemConstantValues(skolem).iterator();tuples.hasNext();) {
		String[] atomsOfTuple = (String[])tuples.next();
		if(atomsOfTuple.length != 1) {
		    Dbg.fail("Skolem relation " + skolem + " is an AlloySet!");
		}
		atom = (AlloyAtom)atomsToAlloyAtoms.get(atomsOfTuple[0]);
		//System.out.println("Atom in skolem set: " + atom);
		if(!instance.containsAtom(atom)) {
		    Dbg.fail("Atom " + atom + " is not in the instance!");
		}
		AlloySet skolemSet = (AlloySet)skolemsToAlloySets.get(skolem);
		instance.addAtomToSet(atom,skolemSet);
	    }
	}
	for (Iterator skolemNames = skolemsToAlloyRelations.keySet().iterator();skolemNames.hasNext();) {
	    String skolem = (String)skolemNames.next();
	    AlloyRelation skolemRelation = (AlloyRelation)skolemsToAlloyRelations.get(skolem);
	    for(Iterator tuples = solutionData.skolemConstantValues(skolem).iterator();tuples.hasNext();) {
		List alloyAtoms = new LinkedList();
		String[] atomsOfTuple = (String[])tuples.next();
		for(int i =0;i<atomsOfTuple.length;i++) {
		    atom = (AlloyAtom)atomsToAlloyAtoms.get(atomsOfTuple[i]);
		    alloyAtoms.add(atom);
		}
		instance.addTupleToRelation(new AlloyTuple(alloyAtoms),skolemRelation);
	    }
	}
    }

    /*
     * Extracts the Module names from types.
     */
    private String getModuleName(String name) {
	//System.out.println(name);
	int lastSlash = name.lastIndexOf("/");
	int firstBracket = name.indexOf("[");
	//System.out.println(firstBracket);
	if(firstBracket > 0) {
	    String nameWithoutBrackets = name.substring(0,firstBracket);
	    return getModuleName(nameWithoutBrackets);
	}

	/*if(lastSlash == -1) {
	    String type = solution Data.typeOfSig(name).toString();
	    int slash = type.lastIn dexOf("/");
	    return type.substring(0, slash);
	    }*/
	return name.substring(0,lastSlash);
    }

    /*
     * Get short name of type without slashes
     */
    /*private String getShortTypeName(String type) {
	int lastslash = type.las tIndexOf("/");
	return type.substring(las tslash+1,type.length());
	}*/

    /*
     * Extract the atom's name. For example, an atom called Man_0
     * will have name Man.
     */
    private String getAtomName(String atomName) {
	int last_ = atomName.lastIndexOf("_");
	return atomName.substring(0,last_);
    }

    /*
     * Extract the atom's index. For example, an atom called Man_0 
     * will have index 0.
     */
    private int getAtomIndex(String atomName) {
	int last_ = atomName.lastIndexOf("_");
	return (new Integer(atomName.substring(last_+1,atomName.length()))).intValue();
    }

    /*
     * Get the relation's module name from sig.
     */
    private String getRelationModuleName(String relationName) {
	int indexOf$ = relationName.lastIndexOf("$");
        String sig = relationName.substring(0,indexOf$);
	
	//System.out.println(sig);
	
	String type = solutionData.typeOfSig(sig).toString();
        return getModuleName(type);
    }

    /*
     * Get the relation's name without the $ qualifier
     */
    private String getShortRelationName(String relationName) {
	int indexOf$ = relationName.lastIndexOf("$");
	String unqualifiedName = relationName.substring(indexOf$+1, relationName.length());
	return unqualifiedName;
    }
	
    /*
     * Extracts the shortened name of Sets and Types. Because the viz
     * is divided into the modules themselves, there should be no
     * ambiguity.
     */
    /* private String getShortName(String sigName) {
	int lastSlash = sigName.lastIndexOf("/");
	return sigName.subString(lastSlash+1,sigName.length());
	}*/
}
